(set-logic QF_UF)
(declare-sort utt$8 0)
(declare-fun Xor (utt$8 utt$8) utt$8)
(declare-fun y0 () utt$8)
(declare-fun y1 () utt$8)
(declare-fun x () utt$8)
(declare-fun y0_n () utt$8)
(declare-fun b () Bool)
(declare-fun bwo1 () utt$8)
(declare-fun bwo2 () utt$8)
(assert (distinct y0 y1 x))
(assert (= x (ite b bwo1 y0)))
(assert (= y0_n y0))
(assert (= bwo1 (Xor x y0)))
(assert (= bwo2 (Xor x y0_n)))
(assert (not (= x bwo2)))
(check-sat)
(exit)
